perm filename DEF1[1,JRA] blob
sn#005824 filedate 1972-10-31 generic text, type T, neo UTF8
00100 ∀(X1,X2,X3,X4) ((((P(X1,X2)∨P(X2,X1))∧(P(X3,X4)∨P(X4,X3)))∧
00200 ((P(X1,X2)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X2)),J(M(N,X1),M(C(N),X4))))
00300 ∧ ((P(X1,X2)∧P(X4,X3))→Q(J(M(N,X4),M(C(N),X2)),J(M(N,X1),M(C(N),X3))))
00400 ∧ ((P(X2,X1)∧P(X4,X3))→Q(J(M(N,X4),M(C(N),X1)),J(M(N,X2),M(C(N),X3))))
00500 ∧ ((P(X2,X1)∧P(X3,X4))→Q(J(M(N,X3),M(C(N),X1)),J(M(N,X2),M(C(N),X4)))))
00600 →R(X1,X2,X3,X4));;
00700 ;
00800 ∀(X1,X2,X3,X4) R(X1,X2,X3,X4);;